T:Type, L:T List. null(L)  (L ~ (firstn(||L||-1;L) @ [last(L)])) 

latex

Definitions	t  T, Top, x:A. B(x), S  T, null(as), b, A, P  Q, ||as||, i>j, , Unit, i<j, P & Q, P  Q, P  Q, , Prop, nth_tl(n;as), last(L), AB, False, {i...j}, l[i], , tl(l), ij, i  j < k, {i..j}
Lemmas	append firstn lastn sq, non neg length, nat wf, length nth tl, le wf, list decomp, nth tl wf, not functionality wrt iff, assert of null, nat plus properties, mul cancel in lt, minus mono wrt lt, add cancel in lt, lt transitivity 2, lt transitivity 1, assert of lt int, lt int eq true elim, length wf1, non nil length, not wf, assert wf, null wf3, top wf